from deslab import *

#def is2controllable(H,G):
#   dump = 'D'
#   Sigma_uc = G.Sigma - G.Sigcon 
#   G_pc = pclosure(G)
#   H_pc = pclosure(H)
#   Haug = H_pc.copy()    
#   Haug = Haug.addstate(dump)   
#   for state in H_pc.X:
#       for event in (Sigma_uc - H_pc.Gamma(state)):
#           Haug = Haug.addtransition([state,event,dump])   
#   L = Haug & G_pc    
#   if L <= H_pc:
#       return True
#   else:
#       return False  


def iscontrollable(H,G):    
    controllable = True
    Sigma_uc = G.Sigma - G.Sigcon
    H0 = product(H,G)   
    for (y,x) in H0.X:
        G_events_uc =  G.Gamma(x) & Sigma_uc
        if not H0.Gamma((y,x)) >= G_events_uc:
            controllable = False
    return controllable

      
def isobservable(H,G):  
    
    def getfirst(stateset):
        for i in stateset:
            return i
    
    def xreached(event,state,auto):
        edges = auto.Graph.out_edges(state,keys=True)
        for edge in edges:
            if edge[2] == event:
                return edge[1]
        return tuple()

    #  X0 = (H._X0(),H.X0(),G.X0())
    #  ou X0 = ( list(H._X0())[0], list(H.X0())[0],   list(G.X0())[0])
    #  pu X0 = (iter(H.X0).next() ,... )
    
    S = [X0]   
    while S <> []:
        state = S.pop()
        
        H1_Gamma = H.Gamma(getfirst(state[0]))
        H2_Gamma = H.Gamma(getfirst(state[1]))
        G_Gamma = G.Gamma(getfirst(state[2]))

        active_events = H1_Gamma.union(H2_Gamma)
        
        for event in active_events:
            if event in G.Sigobs:
                if (event in H1_Gamma) and (event in H2_Gamma) and (event in G_Gamma):
                    X_new = (xreached(event,state[0],H),xreached(event,state[1],H),xreached(event,state[2],G))
                    S.append(X_new)
                elif (event in G.Sigcon) and (event in H1_Gamma) and not(event in H2_Gamma) and (event in G_Gamma):
                    return False
            else:
                if (event in H1_Gamma):
                    X_new = (xreached(event,getfirst(state[0]),H),getfirst(state[1]),getfirst(state[2]))
                    S.append(X_new)
                if (event in H2_Gamma) and (event in G_Gamma):
                    X_new = (getfirst(state[0]),xreached(event,getfirst(state[1]),H),xreached(event,getfirst(state[2]),G))
                    S.append(X_new)
                if (event in G.Sigcon) and (event in H1_Gamma) and not(event in H2_Gamma) and (event in G_Gamma):
                    return False         
    return True
    
    
def obstestcassandras(H,G):  
    
    def getfirst(stateset):
        for i in stateset:
            return i
    
    def xreached(event,state,auto):
        edges = auto.Graph.out_edges(state,keys=True)
        for edge in edges:
            if edge[2] == event:
                return edge[1]
        return tuple()
        
    def createedge(X_new,E_new):
        if not(X_new in X):
            X.append(X_new)
            if X_new <> dead:
                S.append(X_new)            
        
        if not(E_new in E):
            E.append(E_new)
        E_new_string = str(E_new[0]) + ',' + str(E_new[1]) + ',' + str(E_new[2])
        Table.update({E_new: E_new_string})
        
        T_new = (state,E_new,X_new)
        if not(T_new in T):
            T.append(T_new)       

    dead = 'dead'
    
    X0 = (getfirst(H.X0),getfirst(H.X0),getfirst(G.X0))
    X = [X0]
    E = []
    T = []
    Table = {}
    
    S = [X0]   
    while S <> []:
        state = S.pop()        
        
        H1_Gamma = H.Gamma(getfirst(state[0]))
        H2_Gamma = H.Gamma(getfirst(state[1]))
        G_Gamma = G.Gamma(getfirst(state[2]))

        active_events = H1_Gamma.union(H2_Gamma)
        
        for event in active_events:
            if event in G.Sigobs:
                if (event in H1_Gamma) and (event in H2_Gamma) and (event in G_Gamma):                    
                    X_new = (xreached(event,state[0],H),xreached(event,state[1],H),xreached(event,state[2],G))
                    E_new = (event,event,event)
                    createedge(X_new,E_new)
                elif (event in G.Sigcon) and (event in H1_Gamma) and not(event in H2_Gamma) and (event in G_Gamma):
                    X_new = dead
                    E_new = (event,epsilon,event)
                    createedge(X_new,E_new)
            else:
                if (event in H1_Gamma):
                    X_new = (xreached(event,getfirst(state[0]),H),getfirst(state[1]),getfirst(state[2]))
                    E_new = (event,epsilon,epsilon)
                    createedge(X_new,E_new)
                if (event in H2_Gamma) and (event in G_Gamma):
                    X_new = (getfirst(state[0]),xreached(event,getfirst(state[1]),H),xreached(event,getfirst(state[2]),G))
                    E_new = (epsilon,event,event)
                    createedge(X_new,E_new)
                if (event in G.Sigcon) and (event in H1_Gamma) and not(event in H2_Gamma) and (event in G_Gamma):
                    X_new = dead
                    E_new = (event,epsilon,event)
                    createedge(X_new,E_new)
    if dead in X:
        Xm = [dead]
    else:
        Xm = []

    OBSTEST = fsa(X,E,T,X0,Xm,table = Table, name='$ObsTest$')  
    OBSTEST.style='observer'
    OBSTEST.direction='UD'    
    return OBSTEST
    

def supcontrollable(H,G):
    if ispfclosed(H):
        print 'Using Prefix Closed Algorithm'
        Ksupc = supcontrollablepfclosed(H,G)
    else:
        print 'Using General Algorithm'
        Ksupc =  supcontrollablegeneral(H,G) 
       
    if Ksupc <> fsa():
        Ksupc = Ksupc.renamestates('number')
       
    Ksupc= Ksupc.setpar(name ='$K^{\uparrow}^C$')    
    return Ksupc
   

def supcontrollablegeneral(H,G):
    Sigma_uc = G.Sigma - G.Sigcon
    H0 = H&G.setpar(Xm = G.X)
    H_last = fsa()
    H0_changed = True
    while (H0_changed & (H0 <> fsa())):
        H0_changed = False
        H_last = H0
        for (y,x) in H0.X:
            G_events_uc = G.Gamma(x) & Sigma_uc
            if not(G_events_uc <= H0.Gamma((y,x))):
                H0 = H0.deletestate((y,x))
                H0_changed = True                           
        H0 = trim(H0)   
    return H0
   
   
def supcontrollablepfclosed(H,G):
    E_clos = sigmakleeneclos(G.Sigma)   
    Sigma_uc = G.Sigma - G.Sigcon
    E_uc_clos = sigmakleeneclos(Sigma_uc) 
    Ksupc = H-(((G-H)/E_uc_clos)*E_clos)
    return Ksupc
